0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 183 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 92 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 24 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 PiDP
↳17 PiDPToQDPProof (⇔, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
↳21 PiDP
↳22 UsableRulesProof (⇔, 0 ms)
↳23 PiDP
↳24 PiDPToQDPProof (⇒, 0 ms)
↳25 QDP
↳26 QDPSizeChangeProof (⇔, 0 ms)
↳27 YES
↳28 PiDP
↳29 UsableRulesProof (⇔, 0 ms)
↳30 PiDP
↳31 PiDPToQDPProof (⇔, 0 ms)
↳32 QDP
↳33 QDPSizeChangeProof (⇔, 0 ms)
↳34 YES
↳35 PiDP
↳36 PiDPToQDPProof (⇒, 0 ms)
↳37 QDP
↳38 QDPOrderProof (⇔, 107 ms)
↳39 QDP
↳40 DependencyGraphProof (⇔, 0 ms)
↳41 TRUE
REACHD_IN_GGGG(X1, X2, .(X3, X4), X5) → U5_GGGG(X1, X2, X3, X4, X5, memberA_in_ggg(X1, X2, X4))
REACHD_IN_GGGG(X1, X2, .(X3, X4), X5) → MEMBERA_IN_GGG(X1, X2, X4)
MEMBERA_IN_GGG(X1, X2, .(X3, X4)) → U1_GGG(X1, X2, X3, X4, memberA_in_ggg(X1, X2, X4))
MEMBERA_IN_GGG(X1, X2, .(X3, X4)) → MEMBERA_IN_GGG(X1, X2, X4)
REACHD_IN_GGGG(X1, X2, X3, X4) → U6_GGGG(X1, X2, X3, X4, memberB_in_gag(X1, X5, X3))
REACHD_IN_GGGG(X1, X2, X3, X4) → MEMBERB_IN_GAG(X1, X5, X3)
MEMBERB_IN_GAG(X1, X2, .(X3, X4)) → U2_GAG(X1, X2, X3, X4, memberB_in_gag(X1, X2, X4))
MEMBERB_IN_GAG(X1, X2, .(X3, X4)) → MEMBERB_IN_GAG(X1, X2, X4)
REACHD_IN_GGGG(X1, X2, X3, X4) → U7_GGGG(X1, X2, X3, X4, membercB_in_gag(X1, X5, X3))
U7_GGGG(X1, X2, X3, X4, membercB_out_gag(X1, X5, X3)) → U8_GGGG(X1, X2, X3, X4, memberC_in_gg(X5, X4))
U7_GGGG(X1, X2, X3, X4, membercB_out_gag(X1, X5, X3)) → MEMBERC_IN_GG(X5, X4)
MEMBERC_IN_GG(X1, .(X2, X3)) → U3_GG(X1, X2, X3, memberC_in_gg(X1, X3))
MEMBERC_IN_GG(X1, .(X2, X3)) → MEMBERC_IN_GG(X1, X3)
U7_GGGG(X1, X2, X3, X4, membercB_out_gag(X1, X5, X3)) → U9_GGGG(X1, X2, X3, X4, X5, membercC_in_gg(X5, X4))
U9_GGGG(X1, X2, X3, X4, X5, membercC_out_gg(X5, X4)) → U10_GGGG(X1, X2, X3, X4, deleteE_in_gga(X5, X4, X6))
U9_GGGG(X1, X2, X3, X4, X5, membercC_out_gg(X5, X4)) → DELETEE_IN_GGA(X5, X4, X6)
DELETEE_IN_GGA(X1, .(X2, X3), .(X2, X4)) → U4_GGA(X1, X2, X3, X4, deleteE_in_gga(X1, X3, X4))
DELETEE_IN_GGA(X1, .(X2, X3), .(X2, X4)) → DELETEE_IN_GGA(X1, X3, X4)
U9_GGGG(X1, X2, X3, X4, X5, membercC_out_gg(X5, X4)) → U11_GGGG(X1, X2, X3, X4, X5, deletecE_in_gga(X5, X4, X6))
U11_GGGG(X1, X2, X3, X4, X5, deletecE_out_gga(X5, X4, X6)) → U12_GGGG(X1, X2, X3, X4, reachD_in_gggg(X5, X2, X3, X6))
U11_GGGG(X1, X2, X3, X4, X5, deletecE_out_gga(X5, X4, X6)) → REACHD_IN_GGGG(X5, X2, X3, X6)
membercB_in_gag(X1, X2, .(.(X1, .(X2, [])), X3)) → membercB_out_gag(X1, X2, .(.(X1, .(X2, [])), X3))
membercB_in_gag(X1, X2, .(X3, X4)) → U15_gag(X1, X2, X3, X4, membercB_in_gag(X1, X2, X4))
U15_gag(X1, X2, X3, X4, membercB_out_gag(X1, X2, X4)) → membercB_out_gag(X1, X2, .(X3, X4))
membercC_in_gg(X1, .(X1, X2)) → membercC_out_gg(X1, .(X1, X2))
membercC_in_gg(X1, .(X2, X3)) → U16_gg(X1, X2, X3, membercC_in_gg(X1, X3))
U16_gg(X1, X2, X3, membercC_out_gg(X1, X3)) → membercC_out_gg(X1, .(X2, X3))
deletecE_in_gga(X1, .(X1, X2), X2) → deletecE_out_gga(X1, .(X1, X2), X2)
deletecE_in_gga(X1, .(X2, X3), .(X2, X4)) → U22_gga(X1, X2, X3, X4, deletecE_in_gga(X1, X3, X4))
U22_gga(X1, X2, X3, X4, deletecE_out_gga(X1, X3, X4)) → deletecE_out_gga(X1, .(X2, X3), .(X2, X4))
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
REACHD_IN_GGGG(X1, X2, .(X3, X4), X5) → U5_GGGG(X1, X2, X3, X4, X5, memberA_in_ggg(X1, X2, X4))
REACHD_IN_GGGG(X1, X2, .(X3, X4), X5) → MEMBERA_IN_GGG(X1, X2, X4)
MEMBERA_IN_GGG(X1, X2, .(X3, X4)) → U1_GGG(X1, X2, X3, X4, memberA_in_ggg(X1, X2, X4))
MEMBERA_IN_GGG(X1, X2, .(X3, X4)) → MEMBERA_IN_GGG(X1, X2, X4)
REACHD_IN_GGGG(X1, X2, X3, X4) → U6_GGGG(X1, X2, X3, X4, memberB_in_gag(X1, X5, X3))
REACHD_IN_GGGG(X1, X2, X3, X4) → MEMBERB_IN_GAG(X1, X5, X3)
MEMBERB_IN_GAG(X1, X2, .(X3, X4)) → U2_GAG(X1, X2, X3, X4, memberB_in_gag(X1, X2, X4))
MEMBERB_IN_GAG(X1, X2, .(X3, X4)) → MEMBERB_IN_GAG(X1, X2, X4)
REACHD_IN_GGGG(X1, X2, X3, X4) → U7_GGGG(X1, X2, X3, X4, membercB_in_gag(X1, X5, X3))
U7_GGGG(X1, X2, X3, X4, membercB_out_gag(X1, X5, X3)) → U8_GGGG(X1, X2, X3, X4, memberC_in_gg(X5, X4))
U7_GGGG(X1, X2, X3, X4, membercB_out_gag(X1, X5, X3)) → MEMBERC_IN_GG(X5, X4)
MEMBERC_IN_GG(X1, .(X2, X3)) → U3_GG(X1, X2, X3, memberC_in_gg(X1, X3))
MEMBERC_IN_GG(X1, .(X2, X3)) → MEMBERC_IN_GG(X1, X3)
U7_GGGG(X1, X2, X3, X4, membercB_out_gag(X1, X5, X3)) → U9_GGGG(X1, X2, X3, X4, X5, membercC_in_gg(X5, X4))
U9_GGGG(X1, X2, X3, X4, X5, membercC_out_gg(X5, X4)) → U10_GGGG(X1, X2, X3, X4, deleteE_in_gga(X5, X4, X6))
U9_GGGG(X1, X2, X3, X4, X5, membercC_out_gg(X5, X4)) → DELETEE_IN_GGA(X5, X4, X6)
DELETEE_IN_GGA(X1, .(X2, X3), .(X2, X4)) → U4_GGA(X1, X2, X3, X4, deleteE_in_gga(X1, X3, X4))
DELETEE_IN_GGA(X1, .(X2, X3), .(X2, X4)) → DELETEE_IN_GGA(X1, X3, X4)
U9_GGGG(X1, X2, X3, X4, X5, membercC_out_gg(X5, X4)) → U11_GGGG(X1, X2, X3, X4, X5, deletecE_in_gga(X5, X4, X6))
U11_GGGG(X1, X2, X3, X4, X5, deletecE_out_gga(X5, X4, X6)) → U12_GGGG(X1, X2, X3, X4, reachD_in_gggg(X5, X2, X3, X6))
U11_GGGG(X1, X2, X3, X4, X5, deletecE_out_gga(X5, X4, X6)) → REACHD_IN_GGGG(X5, X2, X3, X6)
membercB_in_gag(X1, X2, .(.(X1, .(X2, [])), X3)) → membercB_out_gag(X1, X2, .(.(X1, .(X2, [])), X3))
membercB_in_gag(X1, X2, .(X3, X4)) → U15_gag(X1, X2, X3, X4, membercB_in_gag(X1, X2, X4))
U15_gag(X1, X2, X3, X4, membercB_out_gag(X1, X2, X4)) → membercB_out_gag(X1, X2, .(X3, X4))
membercC_in_gg(X1, .(X1, X2)) → membercC_out_gg(X1, .(X1, X2))
membercC_in_gg(X1, .(X2, X3)) → U16_gg(X1, X2, X3, membercC_in_gg(X1, X3))
U16_gg(X1, X2, X3, membercC_out_gg(X1, X3)) → membercC_out_gg(X1, .(X2, X3))
deletecE_in_gga(X1, .(X1, X2), X2) → deletecE_out_gga(X1, .(X1, X2), X2)
deletecE_in_gga(X1, .(X2, X3), .(X2, X4)) → U22_gga(X1, X2, X3, X4, deletecE_in_gga(X1, X3, X4))
U22_gga(X1, X2, X3, X4, deletecE_out_gga(X1, X3, X4)) → deletecE_out_gga(X1, .(X2, X3), .(X2, X4))
DELETEE_IN_GGA(X1, .(X2, X3), .(X2, X4)) → DELETEE_IN_GGA(X1, X3, X4)
membercB_in_gag(X1, X2, .(.(X1, .(X2, [])), X3)) → membercB_out_gag(X1, X2, .(.(X1, .(X2, [])), X3))
membercB_in_gag(X1, X2, .(X3, X4)) → U15_gag(X1, X2, X3, X4, membercB_in_gag(X1, X2, X4))
U15_gag(X1, X2, X3, X4, membercB_out_gag(X1, X2, X4)) → membercB_out_gag(X1, X2, .(X3, X4))
membercC_in_gg(X1, .(X1, X2)) → membercC_out_gg(X1, .(X1, X2))
membercC_in_gg(X1, .(X2, X3)) → U16_gg(X1, X2, X3, membercC_in_gg(X1, X3))
U16_gg(X1, X2, X3, membercC_out_gg(X1, X3)) → membercC_out_gg(X1, .(X2, X3))
deletecE_in_gga(X1, .(X1, X2), X2) → deletecE_out_gga(X1, .(X1, X2), X2)
deletecE_in_gga(X1, .(X2, X3), .(X2, X4)) → U22_gga(X1, X2, X3, X4, deletecE_in_gga(X1, X3, X4))
U22_gga(X1, X2, X3, X4, deletecE_out_gga(X1, X3, X4)) → deletecE_out_gga(X1, .(X2, X3), .(X2, X4))
DELETEE_IN_GGA(X1, .(X2, X3), .(X2, X4)) → DELETEE_IN_GGA(X1, X3, X4)
DELETEE_IN_GGA(X1, .(X2, X3)) → DELETEE_IN_GGA(X1, X3)
From the DPs we obtained the following set of size-change graphs:
MEMBERC_IN_GG(X1, .(X2, X3)) → MEMBERC_IN_GG(X1, X3)
membercB_in_gag(X1, X2, .(.(X1, .(X2, [])), X3)) → membercB_out_gag(X1, X2, .(.(X1, .(X2, [])), X3))
membercB_in_gag(X1, X2, .(X3, X4)) → U15_gag(X1, X2, X3, X4, membercB_in_gag(X1, X2, X4))
U15_gag(X1, X2, X3, X4, membercB_out_gag(X1, X2, X4)) → membercB_out_gag(X1, X2, .(X3, X4))
membercC_in_gg(X1, .(X1, X2)) → membercC_out_gg(X1, .(X1, X2))
membercC_in_gg(X1, .(X2, X3)) → U16_gg(X1, X2, X3, membercC_in_gg(X1, X3))
U16_gg(X1, X2, X3, membercC_out_gg(X1, X3)) → membercC_out_gg(X1, .(X2, X3))
deletecE_in_gga(X1, .(X1, X2), X2) → deletecE_out_gga(X1, .(X1, X2), X2)
deletecE_in_gga(X1, .(X2, X3), .(X2, X4)) → U22_gga(X1, X2, X3, X4, deletecE_in_gga(X1, X3, X4))
U22_gga(X1, X2, X3, X4, deletecE_out_gga(X1, X3, X4)) → deletecE_out_gga(X1, .(X2, X3), .(X2, X4))
MEMBERC_IN_GG(X1, .(X2, X3)) → MEMBERC_IN_GG(X1, X3)
MEMBERC_IN_GG(X1, .(X2, X3)) → MEMBERC_IN_GG(X1, X3)
From the DPs we obtained the following set of size-change graphs:
MEMBERB_IN_GAG(X1, X2, .(X3, X4)) → MEMBERB_IN_GAG(X1, X2, X4)
membercB_in_gag(X1, X2, .(.(X1, .(X2, [])), X3)) → membercB_out_gag(X1, X2, .(.(X1, .(X2, [])), X3))
membercB_in_gag(X1, X2, .(X3, X4)) → U15_gag(X1, X2, X3, X4, membercB_in_gag(X1, X2, X4))
U15_gag(X1, X2, X3, X4, membercB_out_gag(X1, X2, X4)) → membercB_out_gag(X1, X2, .(X3, X4))
membercC_in_gg(X1, .(X1, X2)) → membercC_out_gg(X1, .(X1, X2))
membercC_in_gg(X1, .(X2, X3)) → U16_gg(X1, X2, X3, membercC_in_gg(X1, X3))
U16_gg(X1, X2, X3, membercC_out_gg(X1, X3)) → membercC_out_gg(X1, .(X2, X3))
deletecE_in_gga(X1, .(X1, X2), X2) → deletecE_out_gga(X1, .(X1, X2), X2)
deletecE_in_gga(X1, .(X2, X3), .(X2, X4)) → U22_gga(X1, X2, X3, X4, deletecE_in_gga(X1, X3, X4))
U22_gga(X1, X2, X3, X4, deletecE_out_gga(X1, X3, X4)) → deletecE_out_gga(X1, .(X2, X3), .(X2, X4))
MEMBERB_IN_GAG(X1, X2, .(X3, X4)) → MEMBERB_IN_GAG(X1, X2, X4)
MEMBERB_IN_GAG(X1, .(X3, X4)) → MEMBERB_IN_GAG(X1, X4)
From the DPs we obtained the following set of size-change graphs:
MEMBERA_IN_GGG(X1, X2, .(X3, X4)) → MEMBERA_IN_GGG(X1, X2, X4)
membercB_in_gag(X1, X2, .(.(X1, .(X2, [])), X3)) → membercB_out_gag(X1, X2, .(.(X1, .(X2, [])), X3))
membercB_in_gag(X1, X2, .(X3, X4)) → U15_gag(X1, X2, X3, X4, membercB_in_gag(X1, X2, X4))
U15_gag(X1, X2, X3, X4, membercB_out_gag(X1, X2, X4)) → membercB_out_gag(X1, X2, .(X3, X4))
membercC_in_gg(X1, .(X1, X2)) → membercC_out_gg(X1, .(X1, X2))
membercC_in_gg(X1, .(X2, X3)) → U16_gg(X1, X2, X3, membercC_in_gg(X1, X3))
U16_gg(X1, X2, X3, membercC_out_gg(X1, X3)) → membercC_out_gg(X1, .(X2, X3))
deletecE_in_gga(X1, .(X1, X2), X2) → deletecE_out_gga(X1, .(X1, X2), X2)
deletecE_in_gga(X1, .(X2, X3), .(X2, X4)) → U22_gga(X1, X2, X3, X4, deletecE_in_gga(X1, X3, X4))
U22_gga(X1, X2, X3, X4, deletecE_out_gga(X1, X3, X4)) → deletecE_out_gga(X1, .(X2, X3), .(X2, X4))
MEMBERA_IN_GGG(X1, X2, .(X3, X4)) → MEMBERA_IN_GGG(X1, X2, X4)
MEMBERA_IN_GGG(X1, X2, .(X3, X4)) → MEMBERA_IN_GGG(X1, X2, X4)
From the DPs we obtained the following set of size-change graphs:
REACHD_IN_GGGG(X1, X2, X3, X4) → U7_GGGG(X1, X2, X3, X4, membercB_in_gag(X1, X5, X3))
U7_GGGG(X1, X2, X3, X4, membercB_out_gag(X1, X5, X3)) → U9_GGGG(X1, X2, X3, X4, X5, membercC_in_gg(X5, X4))
U9_GGGG(X1, X2, X3, X4, X5, membercC_out_gg(X5, X4)) → U11_GGGG(X1, X2, X3, X4, X5, deletecE_in_gga(X5, X4, X6))
U11_GGGG(X1, X2, X3, X4, X5, deletecE_out_gga(X5, X4, X6)) → REACHD_IN_GGGG(X5, X2, X3, X6)
membercB_in_gag(X1, X2, .(.(X1, .(X2, [])), X3)) → membercB_out_gag(X1, X2, .(.(X1, .(X2, [])), X3))
membercB_in_gag(X1, X2, .(X3, X4)) → U15_gag(X1, X2, X3, X4, membercB_in_gag(X1, X2, X4))
U15_gag(X1, X2, X3, X4, membercB_out_gag(X1, X2, X4)) → membercB_out_gag(X1, X2, .(X3, X4))
membercC_in_gg(X1, .(X1, X2)) → membercC_out_gg(X1, .(X1, X2))
membercC_in_gg(X1, .(X2, X3)) → U16_gg(X1, X2, X3, membercC_in_gg(X1, X3))
U16_gg(X1, X2, X3, membercC_out_gg(X1, X3)) → membercC_out_gg(X1, .(X2, X3))
deletecE_in_gga(X1, .(X1, X2), X2) → deletecE_out_gga(X1, .(X1, X2), X2)
deletecE_in_gga(X1, .(X2, X3), .(X2, X4)) → U22_gga(X1, X2, X3, X4, deletecE_in_gga(X1, X3, X4))
U22_gga(X1, X2, X3, X4, deletecE_out_gga(X1, X3, X4)) → deletecE_out_gga(X1, .(X2, X3), .(X2, X4))
REACHD_IN_GGGG(X1, X2, X3, X4) → U7_GGGG(X1, X2, X3, X4, membercB_in_gag(X1, X3))
U7_GGGG(X1, X2, X3, X4, membercB_out_gag(X1, X5, X3)) → U9_GGGG(X1, X2, X3, X4, X5, membercC_in_gg(X5, X4))
U9_GGGG(X1, X2, X3, X4, X5, membercC_out_gg(X5, X4)) → U11_GGGG(X1, X2, X3, X4, X5, deletecE_in_gga(X5, X4))
U11_GGGG(X1, X2, X3, X4, X5, deletecE_out_gga(X5, X4, X6)) → REACHD_IN_GGGG(X5, X2, X3, X6)
membercB_in_gag(X1, .(.(X1, .(X2, [])), X3)) → membercB_out_gag(X1, X2, .(.(X1, .(X2, [])), X3))
membercB_in_gag(X1, .(X3, X4)) → U15_gag(X1, X3, X4, membercB_in_gag(X1, X4))
U15_gag(X1, X3, X4, membercB_out_gag(X1, X2, X4)) → membercB_out_gag(X1, X2, .(X3, X4))
membercC_in_gg(X1, .(X1, X2)) → membercC_out_gg(X1, .(X1, X2))
membercC_in_gg(X1, .(X2, X3)) → U16_gg(X1, X2, X3, membercC_in_gg(X1, X3))
U16_gg(X1, X2, X3, membercC_out_gg(X1, X3)) → membercC_out_gg(X1, .(X2, X3))
deletecE_in_gga(X1, .(X1, X2)) → deletecE_out_gga(X1, .(X1, X2), X2)
deletecE_in_gga(X1, .(X2, X3)) → U22_gga(X1, X2, X3, deletecE_in_gga(X1, X3))
U22_gga(X1, X2, X3, deletecE_out_gga(X1, X3, X4)) → deletecE_out_gga(X1, .(X2, X3), .(X2, X4))
membercB_in_gag(x0, x1)
U15_gag(x0, x1, x2, x3)
membercC_in_gg(x0, x1)
U16_gg(x0, x1, x2, x3)
deletecE_in_gga(x0, x1)
U22_gga(x0, x1, x2, x3)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
U7_GGGG(X1, X2, X3, X4, membercB_out_gag(X1, X5, X3)) → U9_GGGG(X1, X2, X3, X4, X5, membercC_in_gg(X5, X4))
POL(.(x1, x2)) = 1 + x2
POL(REACHD_IN_GGGG(x1, x2, x3, x4)) = 1 + x4
POL(U11_GGGG(x1, x2, x3, x4, x5, x6)) = x6
POL(U15_gag(x1, x2, x3, x4)) = 0
POL(U16_gg(x1, x2, x3, x4)) = 0
POL(U22_gga(x1, x2, x3, x4)) = 1 + x4
POL(U7_GGGG(x1, x2, x3, x4, x5)) = 1 + x4
POL(U9_GGGG(x1, x2, x3, x4, x5, x6)) = x4
POL([]) = 0
POL(deletecE_in_gga(x1, x2)) = x2
POL(deletecE_out_gga(x1, x2, x3)) = 1 + x3
POL(membercB_in_gag(x1, x2)) = 0
POL(membercB_out_gag(x1, x2, x3)) = 0
POL(membercC_in_gg(x1, x2)) = 0
POL(membercC_out_gg(x1, x2)) = 0
deletecE_in_gga(X1, .(X1, X2)) → deletecE_out_gga(X1, .(X1, X2), X2)
deletecE_in_gga(X1, .(X2, X3)) → U22_gga(X1, X2, X3, deletecE_in_gga(X1, X3))
U22_gga(X1, X2, X3, deletecE_out_gga(X1, X3, X4)) → deletecE_out_gga(X1, .(X2, X3), .(X2, X4))
REACHD_IN_GGGG(X1, X2, X3, X4) → U7_GGGG(X1, X2, X3, X4, membercB_in_gag(X1, X3))
U9_GGGG(X1, X2, X3, X4, X5, membercC_out_gg(X5, X4)) → U11_GGGG(X1, X2, X3, X4, X5, deletecE_in_gga(X5, X4))
U11_GGGG(X1, X2, X3, X4, X5, deletecE_out_gga(X5, X4, X6)) → REACHD_IN_GGGG(X5, X2, X3, X6)
membercB_in_gag(X1, .(.(X1, .(X2, [])), X3)) → membercB_out_gag(X1, X2, .(.(X1, .(X2, [])), X3))
membercB_in_gag(X1, .(X3, X4)) → U15_gag(X1, X3, X4, membercB_in_gag(X1, X4))
U15_gag(X1, X3, X4, membercB_out_gag(X1, X2, X4)) → membercB_out_gag(X1, X2, .(X3, X4))
membercC_in_gg(X1, .(X1, X2)) → membercC_out_gg(X1, .(X1, X2))
membercC_in_gg(X1, .(X2, X3)) → U16_gg(X1, X2, X3, membercC_in_gg(X1, X3))
U16_gg(X1, X2, X3, membercC_out_gg(X1, X3)) → membercC_out_gg(X1, .(X2, X3))
deletecE_in_gga(X1, .(X1, X2)) → deletecE_out_gga(X1, .(X1, X2), X2)
deletecE_in_gga(X1, .(X2, X3)) → U22_gga(X1, X2, X3, deletecE_in_gga(X1, X3))
U22_gga(X1, X2, X3, deletecE_out_gga(X1, X3, X4)) → deletecE_out_gga(X1, .(X2, X3), .(X2, X4))
membercB_in_gag(x0, x1)
U15_gag(x0, x1, x2, x3)
membercC_in_gg(x0, x1)
U16_gg(x0, x1, x2, x3)
deletecE_in_gga(x0, x1)
U22_gga(x0, x1, x2, x3)